Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(f,app(s,x))  → app(f,x)
2:    app(g,app(app(cons,0),y))  → app(g,y)
3:    app(g,app(app(cons,app(s,x)),y))  → app(s,x)
4:    app(h,app(app(cons,x),y))  → app(h,app(g,app(app(cons,x),y)))
There are 4 dependency pairs:
5:    APP(f,app(s,x))  → APP(f,x)
6:    APP(g,app(app(cons,0),y))  → APP(g,y)
7:    APP(h,app(app(cons,x),y))  → APP(h,app(g,app(app(cons,x),y)))
8:    APP(h,app(app(cons,x),y))  → APP(g,app(app(cons,x),y))
The approximated dependency graph contains 3 SCCs: {5}, {6} and {7}. Hence the TRS is terminating.
Tyrolean Termination Tool  (0.09 seconds)   ---  May 4, 2006